If A <: B and B <: A, then A = B (subtyping is antisymmetric)
A <: B
B <: A
A = B
A =:= A for all A (equality is reflexive).
A =:= A
A
A =:= A for all A (equality is reflexive). This also provides implicit views A <:< B when A <: B, because (A =:= A) <: (A <:< A) <: (A <:< B).
A <:< B
(A =:= A) <: (A <:< A) <: (A <:< B)